Inference at * 
Iof proof for Lemma lastn wf:


  A:Type, L:(A List), n:. (n  ||L||)  (lastn(n;L)  (A List)) 

latex

 by ((Unfold `lastn` 0) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	lastn(n;L), P  Q, nth_tl(n;as), n - m, A  B, S  T, |g|, , {x:A| B(x)} , ||as||, x:A. B(x), x:AB(x), , type List, s = t, t  T, Type
Lemmas	nth tl wf, le wf, length wf1, nat wf